Om presentation in Cloudozer HQ

Протокол заседаний:

1. В нормальные формы рекурсивных типов верится с трудом, для неподготовленного слушателя, коммутативные диаграммы слабо помогают в этом.
2. Вопрос "зачем писать свой движек" а не писать в Coq + экстрактор можно записывать в FAQ
3. Нужно четко разделять доказательства базовой библиотеки, доказательства
кодировки, доказательства существования изоморфизмов между сигнатурами,
доказательства корректности программы. Когда слишком много кванторов и слова
"доказательства" мозг у слушателей начинает отключаться. С этим нужно что-то думать.
4. Вопрос о практически прямом преобразовании черч кодировки в FPGA примитивы, популярный.
5. Про сертифицированные C компиляторы не все слышали, поэтому это упоминать тоже нужно.
6. Побольше примеров из классического курса математики про брадобреев и
отрицание отрицания и примеры сигнатур, где это имеет значение.

Фото © WIZZARD0